Design By Contract for Rust

Annotate functions and methods with "contracts", using invariants, pre-conditions and post-conditions.

Design by contract is a popular method to augment code with formal interface specifications. These specifications are used to increase the correctness of the code by checking them as assertions at runtime.

pub struct Library {
    available: HashSet<String>,
    lent: HashSet<String>,
}

impl Library {
    fn book_exists(&self, book_id: &str) -> bool {
        self.available.contains(book_id)
            || self.lent.contains(book_id)
    }

    #[debug_requires(!self.book_exists(book_id), "Book IDs are unique")]
    #[debug_ensures(self.available.contains(book_id), "Book now available")]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[ensures(self.lent.len() == old(self.lent.len()), "No lent change")]
    pub fn add_book(&mut self, book_id: &str) {
        self.available.insert(book_id.to_string());
    }

    #[debug_requires(self.book_exists(book_id))]
    #[ensures(ret -> self.available.len() == old(self.available.len()) - 1)]
    #[ensures(ret -> self.lent.len() == old(self.lent.len()) + 1)]
    #[debug_ensures(ret -> self.lent.contains(book_id))]
    #[debug_ensures(!ret -> self.lent.contains(book_id), "Book already lent")]
    pub fn lend(&mut self, book_id: &str) -> bool {
        if self.available.contains(book_id) {
            self.available.remove(book_id);
            self.lent.insert(book_id.to_string());
            true
        } else {
            false
        }
    }

    #[debug_requires(self.lent.contains(book_id), "Can't return a non-lent book")]
    #[ensures(self.lent.len() == old(self.lent.len()) - 1)]
    #[ensures(self.available.len() == old(self.available.len()) + 1)]
    #[debug_ensures(!self.lent.contains(book_id))]
    #[debug_ensures(self.available.contains(book_id), "Book available again")]
    pub fn return_book(&mut self, book_id: &str) {
        self.lent.remove(book_id);
        self.available.insert(book_id.to_string());
    }
}

Attributes

This crate exposes the requires, ensures and invariant attributes.

• requires are checked before a function/method is executed.
• ensures are checked after a function/method ran to completion
• invariants are checked both before and after a function/method ran.

Additionally, all those attributes have versions with different "modes". See the Modes section below.

For traits and trait impls the contract_trait attribute can be used.

More specific information can be found in the crate documentation.

Pseudo-functions and operators

old() function

One unique feature that this crate provides is an old() pseudo-function which allows to perform checks using a value of a parameter before the function call happened. This is only available in ensures attributes.

#[ensures(*x == old(*x) + 1, "after the call `x` was incremented")]
fn incr(x: &mut usize) {
    *x += 1;
}

-> operator

For more complex functions it can be useful to express behaviour using logical implication. Because Rust does not feature an operator for implication, this crate adds this operator for use in attributes.

#[ensures(person_name.is_some() -> ret.contains(person_name.unwrap()))]
fn geeting(person_name: Option<&str>) -> String {
    let mut s = String::from("Hello");
    if let Some(name) = person_name {
        s.push(' ');
        s.push_str(name);
    }
    s.push('!');
    s
}

This operator is right-associative.

Note: Because of the design of syn, it is tricky to add custom operators to be parsed, so this crate performs a rewrite of the TokenStream instead. The rewrite works by separating the expression into a part that's left of the -> operator and the rest on the right side. This means that if a -> b { c } else { d } will not generate the expected code. Explicit grouping using parenthesis or curly-brackets can be used to avoid this.

Modes

All the attributes (requires, ensures, invariant) have debug_* and test_* versions.

• debug_requires/debug_ensures/debug_invariant use debug_assert! internally rather than assert!

• test_requires/test_ensures/test_invariant guard the assert! with an if cfg!(test). This should mostly be used for stating equivalence to "slow but obviously correct" alternative implementations or checks.

  For example, a merge-sort implementation might look like this

  #[test_ensures(is_sorted(input))]
  fn merge_sort<T: Ord + Copy>(input: &mut [T]) {
      // ...
  }
  

Set-up

To install the latest version, add contracts to the dependency section of the Cargo.toml file.

[dependencies]
contracts = "0.6.3"

To then bring all procedural macros into scope, you can add use contracts::*; in all files you plan to use the contract attributes.

Alternatively use the "old-style" of importing macros to have them available project-wide.

#[macro_use]
extern crate contracts;

Configuration

This crate exposes a number of feature flags to configure the assertion behavior.

• disable_contracts - disables all checks and assertions.
• override_debug - changes all contracts (except test_ ones) into debug_* versions
• override_log - changes all contracts (except test_ ones) into a log::error!() call if the condition is violated. No abortion happens.
• mirai_assertions - instead of regular assert! style macros, emit macros used by the MIRAI static analyzer. For more documentation of this usage, head to the MIRAI repo.

TODOs

• implement more contracts for traits.
• add a static analyzer à la SPARK for whole-projects using the contracts to make static assertions.